\begin{tabbing}
ma{-}interface{-}consistent{-}at(${\it es}$;$i$;$X$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it ds}$,$F$ = $X$($i$)\+
\\[0ex]in
\\[0ex]$\forall$$k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\} .
\\[0ex]($\uparrow$$k$ $\in$ dom($F$))
\\[0ex]$\Rightarrow$ \=($\forall$$e$@$i$. (kind($e$) = $k$) $\Rightarrow$ (valtype($e$) $\subseteq$r ($F$($k$).1))\+
\\[0ex]\& ($\forall$$x$:Id. vartype($i$;$x$) $\subseteq$r ${\it ds}$($x$)?Top))
\-\-
\end{tabbing}